es:ES, R:(EE).
(e, e':E. Dec(R(e',e)))
 R => x,y. (x < y)
 (e:E. (e':E. (R(e',e)))  (e':E. es-r-immediate-pred(es;R;e';e))) 

latex

Definitions	{T}, A, P  Q, A c B, x. t(x), P & Q, Dec(P), x(s1,s2), x f y, x,y. t(x;y), R1 => R2, t  T, es-r-immediate-pred(es;R;e';e), x:A. B(x), P  Q, , x:A. B(x), False, x(s)
Lemmas	not wf, decidable cand, decidable existse-causl, es-causl-swellfnd, strongwf-monotone, event system wf, decidable wf, es-causl wf, rel implies wf, es-E wf, rel-immediate-exists